library 
           : '#' 'import' STRING ';'  //import the library by full dll path or DLL name under the Lib folder

     ; 

letDefintion

           : 'var' ID ('<' datatype=ID '>')? variableRange? ('=' expression)? ';'  //user defined datatype is supported using <type>

           | 'var' ID variableRange? '=' recordExpression ';'

           | 'var' ID ('[' expression ']')+ variableRange? ('=' recordExpression)? ';'  //multi-dimensional array is supported

           | ('clock') ID ('[' expression ']')? ';'
                 ;

variableRange

            :':' '{' additiveExpression?'..' additiveExpression? '}'

           ;

recordExpression

            : '[' recordElement (','recordElement)* ']'

           ;

recordElement

           : e1=expression ('(' e2=expression ')')?

           | e1=expression '..' e2=expression

            ;

assertion

           : '#' 'assert' definitionRef            

           (

                       ( '|=' ( '(' | ')' | '[]' | '<>' | ID | STRING | '!' | '?' | '&&' | '||' | '->' | '<->' | '/\\' | '\\/' | '.' | INT )+ )

                                   | 'deadlockfree'  

                                   | 'nonterminating'

                                   | 'divergencefree'

                                   | 'deterministic'

                                   | 'reaches' ID withClause

                                   |  'refines' definitionRef

                                   |  'refines' '<F>' definitionRef

                                   | 'refines' '<FD>' definitionRef

            )

            ';'

           ;

withClause

        : 'with' ('min' | 'max') '(' expression ')'
              ;

definitionRef

           : ID ('('  ')')?

           ;    

define : '#' 'define' ID INT ';'

           | '#' 'define' ID ('true' | 'false') ';'

           | 'enum'  '{' ID (',' ID)*  '}'  ';'

           | '#' 'define' ID conditionalOrExpression ';'

           ;           

block :  '{' statement* expression? '}'

           ;

statement

           : block

           | localVariableDeclaration

           | ifExpression

           | whileExpression

           | expression ';'

           | ';'

           ;

     localVariableDeclaration  
            : 'var' ID ('=' expression)? ';' 

      | 'var' ID '=' recordExpression ';' 

       ;

expression

           : conditionalOrExpression ('=' expression)?

           ;

conditionalOrExpression

          : conditionalAndExpression ( '||' conditionalAndExpression )*

conditionalAndExpression

           : equalityExpression ( '&&' equalityExpression)*

           ;

equalityExpression

            : relationalExpression( ('==' | '!=') relationalExpression)*

            ;

relationalExpression

           : additiveExpression ( ('<' | '>' | '<=' | '>=') additiveExpression)*

            ;

additiveExpression

           : multiplicativeExpression ( ('+' | '-') multiplicativeExpression)*

           ;

multiplicativeExpression

           : unaryExpression ( ('*' | '/' | '%' ) unaryExpression)*

           ;

unaryExpression

           : '+' unaryExpression

           | '-' unaryExpression

           | '!' unaryExpressionNotPlusMinus            

           | unaryExpressionNotPlusMinus '++'       

           | unaryExpressionNotPlusMinus '--'            

           | unaryExpressionNotPlusMinus

           ;

unaryExpressionNotPlusMinus 

           : INT

           | 'true'

           | 'false'

           | 'call' '(' ID (',' conditionalOrExpression)* ')' 

           | new ID '(' (conditionalOrExpression ',' conditionalOrExpression)*)? ')'